COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	On the Algebraic Definition of Programming Languages
C00013 ENDMK
C⊗;
On the Algebraic Definition of Programming Languages
 
M. Broy, P. Pepper, M. Wirsing
 
Technische Universitat Munchen
Institut fur Informatik
Postfach 202420
D-8000 Munchen 2
 
Abstract
 
We outline the algebraic specification of the semantics of programming languages.
Particular emphasis is given to the problem of specifying weakest fixed points
by first order conditional equations.  To cover this issue the theory of
abstract (data) types is slightly extended to particular homomoephusus.
In this framework the semantics of programming languages can be uniquely
specified in a purely algebraic way, using particular modes of a hierarchy
of abstract types.  This approach is demonstrated for a simple procedural
programming language.  Several versions of iterations of increasing complexity
are treated and analyzed with respect to theoretical consequences.  Finally,
as an alternative algebraic technique, transformational semantics is
explained and applied to our examples.
 
l.  Introduction
 
"Semantics is what we have in our heads; as soon as we write it down it is
not semantics anymore." --K. Samuelson (in /Steel, p. 11.)
 
To specify a (denotational) semantics for a programming language means,
strictly speaking, to give rules for translating the programming language into
another language for which a fixed semantics is assumed, i.e. for which a
semantic model is known.  However, as in the case of the specification of data
structures it may be preferable to define the class of semantic models in a more
abstract, algebraic way by means of first order conditional equations.
 
In connection with abstract data types much has been said about the 
advantages of this "abstractness": increased flexibility, concentration on the
essential issues of a given task, easy verifiability, modularization, etc.
When applying these algebraic techniques to the specification of programming
lanuages, we may add the following points to this list of benefits.
 
(1) Since the semantics is given by means of congruence relations on the
language, one has a straightforward notion of "equivalent programs."  Such
equivalences are the basis for any program development process.
 
(11) There is no additional (and too often uncomprehensible) meta-language,
which a programmer has to learn in order to understand the meaning of his
programs.
 
(111) The semantic definition of the language employs the same techniques as
the specification of abstract data types.  This leads to a coherent algebraic
frame for both data structures and control structures (cf. /CIP 811).
 
The obvious advantages of algebraic methods for the specification of programming
languages led to some efforts to extend the theory of abstract types.  Early
work on such algebraic methods (but not yet in the framework of the theory of
abstract types) was done by M. Nicot (cf. for instance /Courcelle, Nicot 781)
In the field of abstract data type there were two pioneering papers on the
specification of programming languages.  In /ADJ 786/ programming languages
are considered as mathematical objects and it is claimed that "programming
languages should be studied in terms of algebraic theories."  In /Ward 771
first order identities are suggested as a defining language to specify the
semantics of programming languages.  
 
However, in both papers one problem is (explicitly) ignored:  First order
identities do not only characterize the classical computable functions; in
connection with partial recursive functions these identities are also fulfilled
by stronger, generally noncomputable functions.  This leads to the problem of
how to express the xxx property of least fixed points in first order logic,
or in other words, to the characterization of the semantic models corresponding
to least fixed points on the class of all (finitely generated) models of the
abstract type under consideration.  This problem is tackled in this paper.
We describe, analyze and contrast the following two approaches:
 
Transformational semantics gives anxious to reduce large parts of a language
to a small, but sufficiently powerful kernal-language, for which the semantics
is assumed to be fixed.  So the problem of characterizing least fixed points of
the extended language is reduced to fixed point theory of the  kernal language.
For instance, in an expression-oriented statement language, each expression
containing statements can be reduced to a pure expression (cf. /Pepper 791),
or in a language containing constructs for concurrent programs every concurrent
program can be transformed into a functionally equivalent sequential
nondeterministic program (cf. /Broy 801).
 
(weakly) terminal semantics specifies a language algebraically by a type T and
defines its semantics to be the isomorphism class of all weakly terminal models
of the type T.  This can be done for a purely applicative "functional programming
language" (cf. /Broy, Wirsing 80a/) or for the language of primitive recurive
functions (cf. /Wirsing, Broy 80/ as well as for procedural programming languages
(cf. /Broy, Wirsing 806/).
 
To demonstrate the fundamental techniques involved in this approach we define
the semantics of a simple procedural programming language first algebraically
by an abstract type and then by transformational semantics.  After a brief
introduction of this sample language and the basic idea, a short definition of
some algebraic notions follows.  Then the sample language is specified as a
hierarchy of absttract types.  Not surprisingly the meaning of all language
constructs can be easily specified in a "sufficiently complete" way except for
the repetition.  For this construct xxx we give three varients of semantic
equation:  construct repetition, where the number of executions is determined
by evaluating the expression  e  "at compilation," static repetition, where the
number of executions is determined before the repetition starts, and
dynamic repetition, where after each execution of  s  the expression  e  is
revaluated.  These three alternatives make the task of specifying the semantics
increasingly more complex as is indicated by the decidability of termination
and by the recursiveness of equality.  We therefore analyze the resulting classes
of semantic models with respect to the syntactical, operational and functtional
equivalence of programs.
 
To give a transformational senatics for our sample language, too, we extend our
type of expressions to a particular form of single, linear primitive recursion,
such that every statement of our sample language can be transformed into a
semantically equivalent expression.  We discuss the similarities and differences
between transformational semantics and purely algebraic semantics and compare
the classes of models arising for our sample languag.e